{-# OPTIONS_GHC -fglasgow-exts #-}
module Synchronizers (Var, string2Var, ValEnv, UpdateEnv, effectiveEnv, applyEnv, Constraint(sync, check), Expression, (<=>), (<|>), (<&>), notc, test, protect, (<.>), intConst, stringConst, valConst, nullConst, letc, lete, forall, exists, exists', one, one', DynCstraint(DynCstraint), ctrace, etrace) where
import DataUpdate
import qualified Data.Set as Set
import qualified Data.Map as Map
import Debug.Trace


data Var = StringVar String | LetVar 
    deriving (Eq, Ord)
string2Var :: String -> Var
string2Var string = StringVar string

instance Show Var where
    showsPrec _ (StringVar v) = showString "$".showString v
    showsPrec _ (LetVar) = showString "$$"

type ValEnv = DValMap Var Value
type UpdateEnv = DValMap Var Update
--data SyncResult = Success UpdateEnv | Conflict
--    deriving (Eq, Show)
--instance Monad SyncResult where
--    (Success env) >>= f = f env
--    Conflict >>= f = Conflict
--    return = Success
--    fail s = Conflict

applyEnv :: UpdateEnv -> ValEnv -> ValEnv
applyEnv uEnv vEnv = unionWithKey (\_ u v -> apply u v) (Prim Null) uEnv vEnv      

effectiveEnv uEnv vEnv = unionWithKey (\_ u v -> effective u v) (getDefaultValue uEnv) uEnv vEnv
    

newID :: DValMap Prim a -> Int
newID dict = 1 + (foldWithKey (\k _ currentMax->case k of {Int i->max currentMax i; otherwise->currentMax;}) 0 dict)

    
newIDv :: Value -> Int
newIDv (Dict dict) = newID dict
newIDv _ = 1

newIDu :: Update -> Int
newIDu (DUpdate dict) = newID dict
newIDu _ = 1

newIDuv :: Update->Value->Int
newIDuv u v = max (newIDv v) (newIDu u) 
  

--union :: Maybe UpdateEnv -> Maybe UpdateEnv -> Maybe UpdateEnv
--union (Just e1) (Just e2) = foldWithKey (\k maybeV env-> maybeV >>= (\v -> return $ env \\ (k, v))) (Just emptyDUpdate) inter 
--    where
--        inter = unionWithKey (\k a b->unionUpdate a b) (Just Void) e1 e2 
--union Nothing _ = Nothing
--union _ Nothing = Nothing

emptyUpdateEnv = empty Void
    

type Check = ValEnv -> Bool
type Eval = ValEnv -> Maybe Value
type Sync = ValEnv -> UpdateEnv -> Maybe UpdateEnv

class (Show a) => Constraint a where
    check :: a -> Check
    sync :: a -> Sync

class (Show a) => Expression a where
    eval :: a -> Eval
    produceVal :: a -> ValEnv -> UpdateEnv -> Maybe Value
    esync :: a -> Var -> Sync
    
    
    
--------------------------------------------------------------------------------
-- v=v

data EqualCstraint = EqualCstraint Var Var

instance Show EqualCstraint where
    showsPrec _ (EqualCstraint v1 v2) = shows v1.showString " = ".shows v2 

instance Constraint EqualCstraint where
    check (EqualCstraint v1 v2) env = 
        (env # v1) == (env # v2)
    sync (EqualCstraint v1 v2) vEnv uEnv = do 
        u <- syncTwoValues (vEnv # v1) 
                    (vEnv # v2) (uEnv # v1) (uEnv # v2) 
        return (uEnv \\ (v1, u) \\ (v2, u))
            
syncTwoValues v1 v2 u1 u2 
    | compatible u1 u2 = 
        Just (u1 <* u2 <* findUpdate v1 new_v)
    | otherwise = Nothing
    where new_v = apply (u1 <* u2) v2

(<=>) :: String -> String -> EqualCstraint
v1 <=> v2 = EqualCstraint (string2Var v1) (string2Var v2) 
infixl 5 <=>

--------------------------------------------------------------------------------
-- and

data (Constraint c1, Constraint c2) => 
    AndCstraint c1 c2 = AndCstraint c1 c2
    
instance (Constraint cstraint1, Constraint cstraint2) => Show (AndCstraint cstraint1 cstraint2) where
    showsPrec _ (AndCstraint c1 c2) = showString "(".shows c1.showString ") = (".shows c2.showString ")" 
    
applyUntilEqual :: (Monad m, Eq a) => (a->m a)->a->m a
applyUntilEqual f v = do
    v' <- f v
    if v' == v then return v' else applyUntilEqual f v'

instance (Constraint c1, Constraint c2) => 
    Constraint (AndCstraint c1 c2) where
    check (AndCstraint c1 c2) env = 
        (check c1 env) && (check c2 env)
    sync (AndCstraint c1 c2) vEnv uEnv = 
        applyUntilEqual f uEnv
        where
        f uEnv' = (sync c1 vEnv uEnv') >>= (sync c2 vEnv)

(<&>) :: (Constraint c1, Constraint c2) => 
    c1 -> c2 -> AndCstraint c1 c2 
c1 <&> c2 = AndCstraint c1 c2
infixl 4 <&>


--------------------------------------------------------------------------------
-- or

data (Constraint cstraint1, Constraint cstraint2) => OrCstraint cstraint1 cstraint2 = OrCstraint cstraint1 cstraint2
    deriving (Show)


instance (Constraint c1, Constraint c2) => Constraint (OrCstraint c1 c2) where
    check (OrCstraint c1 c2) env = (check c1 env) || (check c2 env)
    sync (OrCstraint c1 c2) vEnv uEnv 
        | check c1 vEnv && c1Result /= Nothing = c1Result
        | check c2 vEnv && c2Result /= Nothing = c2Result
        | c1Result /= Nothing = c1Result
        | otherwise = c2Result
        where 
            c1Result = sync c1 vEnv uEnv
            c2Result = sync c2 vEnv uEnv

(<|>) :: (Constraint c1, Constraint c2) => c1 -> c2 -> OrCstraint c1 c2
c1 <|> c2 = OrCstraint c1 c2
infixl 3 <|>

--------------------------------------------------------------------------------
-- forall
data (Constraint c) => ForAllCstraint c = ForAllCstraint Var Var c
    deriving (Show)
    
dictReplacedCall :: Var->Prim->Var->(ValEnv->UpdateEnv->Maybe UpdateEnv)->ValEnv->UpdateEnv->Maybe UpdateEnv
dictReplacedCall dvar key vvar f vEnv uEnv = do
    innerUpdate <- getu (uEnv # dvar) key
    innerValue <- case getv (vEnv # dvar) key of
                        Just v -> return v
                        otherwise -> return $ Prim Null
    uEnv' <- return $ uEnv \\ (vvar, innerUpdate)
    vEnv' <- return $ vEnv \\ (vvar, innerValue)
    uEnv' <- f vEnv' uEnv'
    let u = uEnv' # vvar in return $ uEnv' \\ (dvar, replaceInDict key (uEnv' # dvar) u) \\ (vvar, uEnv # vvar)
    
maybe2bool :: Maybe Bool -> Bool
maybe2bool (Just b) = b
maybe2bool Nothing = False

instance (Constraint c) => Constraint (ForAllCstraint c) where
    check (ForAllCstraint dvar vvar c) env =
        let 
            result = do
                dict <- getDict (env # dvar) 
                return $ foldWithKey (\_ v b-> check c (env \\ (vvar, v)) && b) True dict          
        in maybe2bool result
    sync (ForAllCstraint dvar vvar c) vEnv uEnv = applyUntilEqual f (uEnv \\ (dvar, uEnv # dvar <* DUpdate emptyDUpdate))
        where
            f uEnv = Set.fold (\k env->env >>= innerSync k) (Just uEnv) allKeys
            allKeys = (Set.union (dict2Set $ getDict (vEnv # dvar)) (dict2Set $ getUDict (uEnv # dvar))) 
            innerSync k = dictReplacedCall dvar k vvar (sync innerCstraint) vEnv
            innerCstraint = c <|> (TestCstraint $ ExprCstraint vvar (ConstExpr $ Prim Null))  
            dict2Set (Just dict) = keysSet dict
            dict2Set Nothing = Set.empty
              
forall :: (Constraint c) => 
    String -> String -> c -> ForAllCstraint c 
forall d v c = 
    ForAllCstraint (string2Var d) (string2Var v) c

--------------------------------------------------------------------------------
-- exists

data (Constraint c) => ExistsCstraint c = ExistsCstraint Var Var c
    deriving (Show)
    
findKey c dvar vvar env = do
    dict <- getDict (env # dvar)
    foldWithKey (\k v curK-> if curK == Nothing && check c (env \\ (vvar, v)) then Just k else curK) Nothing dict 

instance (Constraint c) => Constraint (ExistsCstraint c) where
    check (ExistsCstraint dvar vvar c) env = findKey c dvar vvar env /= Nothing
--        let result = 
--                dict <- getDict (env # dvar) 
--                return $ foldWithKey (\_ v b-> check c (env \\ (vvar, v)) || b) False dict          
--        in maybe2bool result
    sync cstraint@(ExistsCstraint dvar vvar c) vEnv uEnv 
        | check cstraint (applyEnv uEnv vEnv) = Just uEnv
        | otherwise = addAndSyncNewEntry dvar vvar c vEnv uEnv
                
addAndSyncNewEntry dvar vvar c vEnv uEnv =  
    dictReplacedCall dvar (Int theID) vvar innerCstraint vEnv uEnv
    where
        theID = newIDuv (uEnv # dvar) (vEnv # dvar)
        innerCstraint = nonNullSync c vvar
nonNullSync c vvar = sync $ AndCstraint c (NotCstraint (ExprCstraint vvar $ ConstExpr (Prim Null)))

exists :: (Constraint c) => 
    String -> String -> c -> ExistsCstraint c 
exists d v c = 
    ExistsCstraint (string2Var d) (string2Var v) c


--------------------------------------------------------------------------------
-- one

data (Constraint c) => OneCstraint c = OneCstraint Var Var c
    deriving (Show)

countSatisfied c dvar vvar env = do
    dict <- getDict (env # dvar)
    return $ 
        foldWithKey (\k v count->if check c (env \\ (vvar, v)) then count + 1 else count) 0 dict

instance (Constraint c) => Constraint (OneCstraint c) where
    check (OneCstraint dvar vvar c) env = countSatisfied c dvar vvar env == Just 1 
    sync cstraint@(OneCstraint dvar vvar c) vEnv uEnv
        | countSatisfied c dvar vvar (applyEnv uEnv vEnv) == Just 1 = Just uEnv
        | countSatisfied c dvar vvar (applyEnv uEnv vEnv) == Just 0 = addAndSyncNewEntry dvar vvar c vEnv uEnv
        | otherwise = Nothing  

one :: (Constraint c) => String -> String -> c -> OneCstraint c
one d v c = 
    OneCstraint (string2Var d) (string2Var v) c


--------------------------------------------------------------------------------
-- one expression

--data (Constraint c) => OneExpr c = OneExpr Var Var c
--    deriving (Show)
--
--instance (Constraint c) => Expression (OneExpr c) where
--    eval (OneExpr dvar vvar c) env  
--        | countSatisfied c dvar vvar env == Just 1 = do
--            key <- findKey c dvar vvar env
--            return $ Prim key
--        | otherwise = Nothing
--    produceVal (OneExpr dvar vvar c) vEnv uEnv = 
--        case eval (OneExpr dvar vvar c) vEnv of
--            Just key -> Just key
--            Nothing ->  Just $ Prim Null  
--    esync cstraint@(OneExpr dvar vvar c) kvar vEnv uEnv
--        | (uEnv # kvar) == Void = unfixedKey
--        | otherwise = fixedKey
--        where
--            unfixedKey :: Maybe UpdateEnv
--            unfixedKey = 
--                if countSatisfiedForUEnv uEnv == Just 1
--                    then do
--                        key <- findKey c dvar vvar (applyEnv uEnv vEnv) 
--                        return $ replaceKeyIfNecessary uEnv vEnv key
--                    else if countSatisfiedForUEnv uEnv == Just 0 
--                            then do
--                                uEnv' <- dictReplacedCall dvar newID vvar innerCstraint vEnv uEnv
--                                return $ replaceKeyIfNecessary uEnv' vEnv newID
--                            else Nothing
--            replaceKeyIfNecessary :: UpdateEnv -> ValEnv -> Prim -> UpdateEnv 
--            replaceKeyIfNecessary uEnv vEnv key = if vEnv # kvar == Prim key then uEnv else uEnv \\ (kvar, PUpdate $ key)
--            newID = Int $ newIDuv (uEnv # dvar) (vEnv # dvar)
--            fixedKey :: Maybe UpdateEnv
--            fixedKey = do
--                let keyValue = apply (uEnv # kvar) (vEnv # kvar)
--                key <- case keyValue of {Prim k -> Just k; otherwise->Nothing}
--                uEnv' <- dictReplacedCall dvar key vvar innerCstraint vEnv uEnv
--                if countSatisfiedForUEnv uEnv' == Just 1 then return uEnv' else fail "" 
--            countSatisfiedForUEnv ue = countSatisfied c dvar vvar (applyEnv ue vEnv) 
--            innerCstraint = nonNullSync c vvar
--            
--eone :: (Constraint c) => String -> String -> c -> OneExpr c
--eone d v c = 
--    OneExpr (string2Var d) (string2Var v) c

data (Constraint c) => One'Cstraint c = One'Cstraint Var Var Var c
    deriving (Show)

instance (Constraint c) => Constraint (One'Cstraint c) where
    check (One'Cstraint kvar dvar vvar c) env  
        | countSatisfied c dvar vvar env == Just 1 = maybe2bool $ do
            key <- getPrim $ env # kvar
            value <- getv (env # dvar) key   
            return $ check c (env \\ (vvar, value))
        | otherwise = False
        where
            maybe2bool (Just False) = False
            maybe2bool (Just _) = True
            maybe2bool Nothing = False
    sync cstraint@(One'Cstraint kvar dvar vvar c) vEnv uEnv
        | (uEnv # kvar) == Void = unfixedKey
        | otherwise = fixedKey
        where
            unfixedKey :: Maybe UpdateEnv
            unfixedKey = 
                if countSatisfiedForUEnv uEnv == Just 1
                    then do
                        key <- findKey c dvar vvar (applyEnv uEnv vEnv) 
                        return $ replaceKeyIfNecessary uEnv vEnv key
                    else if countSatisfiedForUEnv uEnv == Just 0 
                            then do
                                uEnv' <- dictReplacedCall dvar newID vvar innerCstraint vEnv uEnv
                                return $ replaceKeyIfNecessary uEnv' vEnv newID
                            else Nothing
            replaceKeyIfNecessary :: UpdateEnv -> ValEnv -> Prim -> UpdateEnv 
            replaceKeyIfNecessary uEnv vEnv key = if vEnv # kvar == Prim key then uEnv else uEnv \\ (kvar, PUpdate $ key)
            newID = Int $ newIDuv (uEnv # dvar) (vEnv # dvar)
            fixedKey :: Maybe UpdateEnv
            fixedKey = do
                let keyValue = apply (uEnv # kvar) (vEnv # kvar)
                key <- case keyValue of {Prim k -> Just k; otherwise->Nothing}
                uEnv' <- dictReplacedCall dvar key vvar innerCstraint vEnv uEnv
                if countSatisfiedForUEnv uEnv' == Just 1 then return uEnv' else fail "" 
            countSatisfiedForUEnv ue = countSatisfied c dvar vvar (applyEnv ue vEnv) 
            innerCstraint = nonNullSync c vvar
            
one' :: (Constraint c) => String -> String -> String -> c -> One'Cstraint c
one' k d v c = 
    One'Cstraint (string2Var k) (string2Var d) (string2Var v) c

--------------------------------------------------------------------------------
-- exists!

data (Constraint c) => Exists'Cstraint c = Exists'Cstraint Var Var c
    deriving (Show)

instance (Constraint c) => Constraint (Exists'Cstraint c) where
    check (Exists'Cstraint dvar vvar c) env = check (ExistsCstraint dvar vvar c) env
    sync (Exists'Cstraint dvar vvar c) vEnv uEnv =
        case lastKey of
            Just k -> dictReplacedCall dvar k vvar innerCstraint vEnv uEnv
            otherwise -> sync (ExistsCstraint dvar vvar c) vEnv uEnv
        where
           lastKey = findKey c dvar vvar vEnv
           innerCstraint = nonNullSync c vvar

exists' :: (Constraint c) => String -> String -> c -> Exists'Cstraint c 
exists' d v c = Exists'Cstraint (string2Var d) (string2Var v) c


--------------------------------------------------------------------------------
-- test

data (Constraint c) => TestCstraint c = TestCstraint c
    deriving (Show)
    
instance (Constraint c) => Constraint (TestCstraint c) where
    check (TestCstraint c) env = check c env
    sync (TestCstraint c) vEnv uEnv  
        | check c (applyEnv uEnv vEnv) = Just uEnv
        | otherwise = Nothing

test :: Constraint c => c -> TestCstraint c        
test c = TestCstraint c

--------------------------------------------------------------------------------
-- protect

data (Constraint c) => ProtectCstraint c = ProtectCstraint Var c
    deriving (Show)
    
instance (Constraint c) => Constraint (ProtectCstraint c) where
    check (ProtectCstraint var c) env = check c env
    sync (ProtectCstraint var c) vEnv uEnv = do
        uEnv' <- sync c vEnv uEnv
        if apply (uEnv' # var) (vEnv # var) == apply (uEnv # var) (vEnv # var) 
            then return uEnv'
            else fail ""  

protect :: (Constraint c) => 
    String -> c -> ProtectCstraint c
protect var c = ProtectCstraint (string2Var var) c
                
--------------------------------------------------------------------------------
-- not

data (Constraint c) => NotCstraint c = NotCstraint c
    deriving (Show)
    
instance (Constraint c) => Constraint (NotCstraint c) where
    check (NotCstraint c) env = not (check c env)
    sync (NotCstraint c) vEnv uEnv  
        | check c (applyEnv uEnv vEnv) = Nothing
        | otherwise = Just uEnv
                 

notc :: Constraint c => c -> NotCstraint c
notc c = NotCstraint c
--------------------------------------------------------------------------------
-- let
    
data (Expression expr, Constraint cst) => 
    LetCstraint expr cst = LetCstraint Var expr cst
    
instance (Expression expr, Constraint cstraint) => Show (LetCstraint expr cstraint) where
    showsPrec _ (LetCstraint var expr cstraint) = showString "letc ".shows var.showString " = (".shows expr.showString ") in (".shows cstraint.showString ")"
    
--trace ("\n\n" ++ show (LetCstraint var expr cstraint) ++ "\n values: " ++ show (vEnv) ++ "\n updates: " ++ show uEnv) $
    
instance (Expression expr, Constraint cstraint) => 
    Constraint (LetCstraint expr cstraint) where
    check (LetCstraint var expr cst) env = 
        let evalResult = eval expr env in check' evalResult
        where 
            check' (Just v) = check cst (env \\ (var, v))
            check' Nothing = False
    sync (LetCstraint var expr cstraint) vEnv uEnv = do
        replaced <- produceVal expr vEnv uEnv 
        (_, _, result) <- applyUntilEqual invokeOnce 
                            (replaced, Void, uEnv)
        return result
        where
        invokeOnce e = invokeExpr e >>= invokeCstraint  
        invokeExpr (varVal, varUpdate, uEnv') = do
            replaced <- produceVal expr vEnv uEnv 
            replaced' <- produceVal expr vEnv uEnv'
            if replaced == replaced'
                then invoke (ExprCstraint LetVar expr) LetVar (varVal, varUpdate, uEnv')
                else fail "the inner value has been changed"
        invokeCstraint = invoke cstraint var
        invoke c var (v, u, uEnv) = do 
            resultEnv <- 
                sync c (vEnv \\ (var, v)) (uEnv \\ (var, u))
            return (v, resultEnv # var, 
                     resultEnv \\ (var, uEnv # var))
            

letc :: (Expression e, Constraint c) => 
    String -> e -> c -> LetCstraint e c             
letc varName expr cstraint = LetCstraint (string2Var varName) expr cstraint
    
--------------------------------------------------------------------------------
-- expression lifter
-- var must not appears in expr

data (Expression expr) => 
    ExprCstraint expr = ExprCstraint Var expr
    deriving (Show)

instance (Expression expr) => 
    Constraint (ExprCstraint expr) where
    check (ExprCstraint var e) env = case eval e env of
        Just c -> c == env # var
        Nothing -> False
    sync (ExprCstraint var e) vEnv uEnv = 
        esync e var vEnv uEnv 


--------------------------------------------------------------------------------
-- const
data ConstExpr = ConstExpr Value
    
instance Show ConstExpr where
    showsPrec _ (ConstExpr c) = shows c
    

instance Expression ConstExpr where
    eval (ConstExpr c) _ = Just c
    produceVal (ConstExpr c) _ _  = Just c 
    esync (ConstExpr c) var vEnv uEnv 
        | compatible u (uEnv # var) = 
            return (uEnv \\ (var, u <* uEnv # var))
        | otherwise = fail ""
        where
            u = findUpdate (apply (uEnv # var) (vEnv # var)) c 

intConst :: Int -> ConstExpr
intConst i = ConstExpr (Prim $ Int i)
stringConst :: String -> ConstExpr
stringConst s = ConstExpr (Prim $ String s)
nullConst :: ConstExpr
nullConst = ConstExpr (Prim Null)
valConst v = ConstExpr v

--------------------------------------------------------------------------------
-- d.k
data DictGetExpr = DictGetExpr Var Var

instance Show DictGetExpr where
    showsPrec _ (DictGetExpr d k) = shows d.showString ".".shows k

    
getv :: Value -> Prim -> Maybe Value
getv (Dict dict) key = Just $ dict # key
getv _ key = Nothing

getu :: Update -> Prim -> Maybe Update
getu (DUpdate dict) key = Just $ dict # key
getu (PUpdate _) key = Nothing
getu Void key = Just Void

getPrim :: Value -> Maybe Prim
getPrim (Prim v) = Just v
getPrim _ = Nothing

getDict :: Value -> Maybe Dict
getDict (Dict v) = Just v
getDict _ = Nothing

getUDict :: Update -> Maybe DUpdate
getUDict (DUpdate v) = Just v
getUDict _ = Nothing


replaceInDict newKey (DUpdate d) u = DUpdate (d \\ (newKey, u))
replaceInDict newKey _ u =  DUpdate (emptyDUpdate \\ (newKey, u))

    
instance Expression DictGetExpr where
    eval (DictGetExpr dvar kvar) env = do
        key  <- getPrim (env # kvar)
        getv (env # dvar) key
    produceVal (DictGetExpr dvar kvar) vEnv uEnv = do
        newKey <- getPrim (apply (uEnv # kvar) (vEnv # kvar))
        case getDict (vEnv # dvar) of
            Just dict -> return $ dict # newKey
            Nothing -> return $ Prim Null
    esync cstraint@(DictGetExpr dvar kvar) var vEnv uEnv = do
        newKey <- getPrim (apply (uEnv # kvar) (vEnv # kvar))
        process newKey
        
        where
        process newKey 
            | newKey == Null && uEnv # kvar == Void = 
                let insertedKey = newIDuv (uEnv # dvar) (vEnv # dvar) 
                    keyUpdate = PUpdate (Int insertedKey) in
                esync cstraint var vEnv (uEnv \\ (kvar, keyUpdate))
            | newKey == Null                      = fail ""
            | otherwise                          = process' newKey
        process' newKey = do
            innerUpdate <- getu (uEnv # dvar) newKey
            innerValue <- case getv (vEnv # dvar) newKey of
                                Just v -> return v
                                otherwise -> return $ Prim Null
            u <- syncTwoValues (vEnv # var) innerValue (uEnv # var) innerUpdate
            uEnv <- return $ uEnv \\ (var, u) 
            uEnv <- return $ uEnv \\ (dvar, replaceInDict newKey (uEnv # dvar) u)
            if u == uEnv # var && u == innerUpdate 
                then return uEnv
                else return $ uEnv \\ (kvar, PUpdate newKey)                                
                
(<.>) :: String -> String -> DictGetExpr
d <.> k = DictGetExpr (string2Var d) (string2Var k)
infixl 6 <.>
--------------------------------------------------------------------------------
-- Let Expr

data (Expression expr1, Expression expr2) => LetExpr expr1 expr2 = LetExpr Var expr1 expr2

instance (Expression expr, Expression expr2) => Show (LetExpr expr expr2) where
    showsPrec _ (LetExpr var expr cstraint) = showString "lete ".shows var.showString " = (".shows expr.showString ") in (".shows cstraint.showString ")"

instance (Expression expr1, Expression expr2) => Expression (LetExpr expr1 expr2) where
    eval (LetExpr var expr1 expr2) env = do  
        v <- eval expr1 env 
        eval expr2 (env \\ (var, v))
    produceVal (LetExpr var expr1 expr2) vEnv uEnv = do
        innerVal <- produceVal (expr1) vEnv uEnv
        let vEnv' = vEnv \\ (var, innerVal)
        uEnv' <- esync expr1 var vEnv' uEnv
        produceVal (expr2) vEnv' uEnv'
    esync (LetExpr var1 expr1 expr2) var2 vEnv uEnv =
        sync (LetCstraint var1 expr1 (ExprCstraint var2 expr2)) vEnv uEnv

lete :: (Expression expr1, Expression expr2) => 
    String -> expr1 -> expr2 -> LetExpr expr1 expr2            
lete varName expr1 expr2 = LetExpr (string2Var varName) expr1 expr2

--------------------------------------------------------------------------------
-- relation definition and call

data DynCstraint = forall a. Constraint a => DynCstraint a

instance Show DynCstraint
    where
    showsPrec _ _ = showString "RelationReference"    
    
instance Constraint DynCstraint
    where
        check (DynCstraint c) = check c
        sync (DynCstraint c) = sync c

--type RelationDefs = Map.Map String (DynCstraint, [Var])
--
--data RelationRef = RelationRef DynCstraint [Var] [Var]
--    deriving Show
--    
--replaceVars oldvars newvars env = foldl (\env' (old, new)-> env' \\ (new, env # old)) (deletevars env oldvars) (zip oldvars newvars)
--    where  
--        deletevars = foldl (\env' var -> delete var env')
--        
--instance Constraint RelationRef where
--    check (RelationRef dynCstraint paras args) env = 
--        check dynCstraint (replaceVars args paras env)
--    sync (RelationRef dynCstraint paras args) vEnv uEnv =
--        case innerResult of 
--            Just env' -> Just $ replaceVars paras args env'
--            Nothing -> Nothing 
--        where
--            innerResult = sync dynCstraint (replaceVars args paras vEnv) (replaceVars args paras uEnv)

            
--_main a b  = (a <=> b) <&> DynCstraint (_main a b)
 
         
--------------------------------------------------------------------------------
-- Traces
env2TraceMsg :: (Show v, Show k, Ord k) => DValMap k v -> Maybe (Set.Set k) -> String
env2TraceMsg env (Just vars) = Set.fold (\v msg->msg ++ show v ++ ":" ++ show (env # v) ++ ",") "" vars
env2TraceMsg env Nothing = env2TraceMsg env (Just $ keysSet env)
    
syncResult2TraceMsg (Just env) vars = env2TraceMsg env vars
syncResult2TraceMsg Nothing _ = "Synchronization failed!"

data (Expression expr) => TraceExpr expr = TraceExpr (Maybe (Set.Set Var)) String expr

instance (Expression expr) => Show (TraceExpr expr) where
    showsPrec n (TraceExpr _ _ expr) = showsPrec n expr

instance (Expression expr) => Expression (TraceExpr expr) where
    eval (TraceExpr vars msg expr) env = 
        trace traceMsg result
        where
            result = eval expr env
            traceMsg = msg ++ " eval() called.\n" ++ evalMsg env vars result
    produceVal (TraceExpr _ _ expr) = produceVal expr             
    esync (TraceExpr vars msg expr) var vEnv uEnv =
        trace traceMsg result
        where 
            result = esync expr var vEnv uEnv
            traceMsg = msg ++ " sync() called.\n" ++ syncMsg vEnv uEnv vars result 

noVars (Just vars) = Set.null vars
noVars Nothing = False
evalMsg :: (Show r) => ValEnv -> Maybe (Set.Set Var) -> r -> String
evalMsg env vars result 
    | not $ noVars vars = "input: " ++ env2TraceMsg env vars ++ "\noutput: " ++ show result ++ "\n"
    | otherwise = ""
syncMsg vEnv uEnv vars result 
    | not $ noVars vars = "input values: " ++ env2TraceMsg vEnv vars ++ 
        "\ninput updates: " ++ env2TraceMsg uEnv vars ++ 
        "\noutput updates: " ++ syncResult2TraceMsg result vars ++ "\n"
    | otherwise = ""


etrace :: (Expression expr) => String -> Maybe [String] -> expr -> TraceExpr expr 
etrace msg vars expr = TraceExpr (maybeMap (Set.fromList.(map string2Var)) vars) msg expr

maybeMap :: (a->b)->Maybe a->Maybe b
maybeMap f (Just a) = Just (f a)
maybeMap _ Nothing = Nothing  

data (Constraint cstraint) => TraceCstraint cstraint = TraceCstraint (Maybe (Set.Set Var)) String cstraint

instance (Constraint cstraint) => Show (TraceCstraint cstraint) where
    showsPrec n (TraceCstraint _ _ cstraint) = showsPrec n cstraint

instance (Constraint cstraint) => Constraint (TraceCstraint cstraint) where
    check (TraceCstraint vars msg cstraint) env = 
        trace traceMsg result
        where
            result = check cstraint env
            traceMsg = msg ++ "eval() called.\n" ++ evalMsg env vars result 
    sync (TraceCstraint vars msg cstraint) vEnv uEnv =
        trace traceMsg result
        where 
            result = sync cstraint vEnv uEnv
            traceMsg = msg ++ " sync() called.\n" ++ syncMsg vEnv uEnv vars result

ctrace :: (Constraint cstraint) => String -> Maybe [String] -> cstraint -> TraceCstraint cstraint 
ctrace msg vars cstraint = TraceCstraint (maybeMap (Set.fromList.(map string2Var)) vars) msg cstraint